0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 85 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 26 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 26 ms)
↳12 QDP
↳13 UsableRulesReductionPairsProof (⇔, 59 ms)
↳14 QDP
↳15 MRRProof (⇔, 0 ms)
↳16 QDP
↳17 PisEmptyProof (⇔, 0 ms)
↳18 YES
flatA_in_ga([], []) → flatA_out_ga([], [])
flatA_in_ga(.([], []), []) → flatA_out_ga(.([], []), [])
flatA_in_ga(.([], .([], T16)), T18) → U1_ga(T16, T18, flatA_in_ga(T16, T18))
flatA_in_ga(.([], .(.(T35, T36), T37)), .(T35, T39)) → U2_ga(T35, T36, T37, T39, flatA_in_ga(.(T36, T37), T39))
flatA_in_ga(.(.(T44, []), T57), .(T44, T59)) → U3_ga(T44, T57, T59, flatA_in_ga(T57, T59))
flatA_in_ga(.(.(T44, .(T68, T69)), T70), .(T44, .(T68, T72))) → U4_ga(T44, T68, T69, T70, T72, flatA_in_ga(.(T69, T70), T72))
U4_ga(T44, T68, T69, T70, T72, flatA_out_ga(.(T69, T70), T72)) → flatA_out_ga(.(.(T44, .(T68, T69)), T70), .(T44, .(T68, T72)))
U3_ga(T44, T57, T59, flatA_out_ga(T57, T59)) → flatA_out_ga(.(.(T44, []), T57), .(T44, T59))
U2_ga(T35, T36, T37, T39, flatA_out_ga(.(T36, T37), T39)) → flatA_out_ga(.([], .(.(T35, T36), T37)), .(T35, T39))
U1_ga(T16, T18, flatA_out_ga(T16, T18)) → flatA_out_ga(.([], .([], T16)), T18)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
flatA_in_ga([], []) → flatA_out_ga([], [])
flatA_in_ga(.([], []), []) → flatA_out_ga(.([], []), [])
flatA_in_ga(.([], .([], T16)), T18) → U1_ga(T16, T18, flatA_in_ga(T16, T18))
flatA_in_ga(.([], .(.(T35, T36), T37)), .(T35, T39)) → U2_ga(T35, T36, T37, T39, flatA_in_ga(.(T36, T37), T39))
flatA_in_ga(.(.(T44, []), T57), .(T44, T59)) → U3_ga(T44, T57, T59, flatA_in_ga(T57, T59))
flatA_in_ga(.(.(T44, .(T68, T69)), T70), .(T44, .(T68, T72))) → U4_ga(T44, T68, T69, T70, T72, flatA_in_ga(.(T69, T70), T72))
U4_ga(T44, T68, T69, T70, T72, flatA_out_ga(.(T69, T70), T72)) → flatA_out_ga(.(.(T44, .(T68, T69)), T70), .(T44, .(T68, T72)))
U3_ga(T44, T57, T59, flatA_out_ga(T57, T59)) → flatA_out_ga(.(.(T44, []), T57), .(T44, T59))
U2_ga(T35, T36, T37, T39, flatA_out_ga(.(T36, T37), T39)) → flatA_out_ga(.([], .(.(T35, T36), T37)), .(T35, T39))
U1_ga(T16, T18, flatA_out_ga(T16, T18)) → flatA_out_ga(.([], .([], T16)), T18)
FLATA_IN_GA(.([], .([], T16)), T18) → U1_GA(T16, T18, flatA_in_ga(T16, T18))
FLATA_IN_GA(.([], .([], T16)), T18) → FLATA_IN_GA(T16, T18)
FLATA_IN_GA(.([], .(.(T35, T36), T37)), .(T35, T39)) → U2_GA(T35, T36, T37, T39, flatA_in_ga(.(T36, T37), T39))
FLATA_IN_GA(.([], .(.(T35, T36), T37)), .(T35, T39)) → FLATA_IN_GA(.(T36, T37), T39)
FLATA_IN_GA(.(.(T44, []), T57), .(T44, T59)) → U3_GA(T44, T57, T59, flatA_in_ga(T57, T59))
FLATA_IN_GA(.(.(T44, []), T57), .(T44, T59)) → FLATA_IN_GA(T57, T59)
FLATA_IN_GA(.(.(T44, .(T68, T69)), T70), .(T44, .(T68, T72))) → U4_GA(T44, T68, T69, T70, T72, flatA_in_ga(.(T69, T70), T72))
FLATA_IN_GA(.(.(T44, .(T68, T69)), T70), .(T44, .(T68, T72))) → FLATA_IN_GA(.(T69, T70), T72)
flatA_in_ga([], []) → flatA_out_ga([], [])
flatA_in_ga(.([], []), []) → flatA_out_ga(.([], []), [])
flatA_in_ga(.([], .([], T16)), T18) → U1_ga(T16, T18, flatA_in_ga(T16, T18))
flatA_in_ga(.([], .(.(T35, T36), T37)), .(T35, T39)) → U2_ga(T35, T36, T37, T39, flatA_in_ga(.(T36, T37), T39))
flatA_in_ga(.(.(T44, []), T57), .(T44, T59)) → U3_ga(T44, T57, T59, flatA_in_ga(T57, T59))
flatA_in_ga(.(.(T44, .(T68, T69)), T70), .(T44, .(T68, T72))) → U4_ga(T44, T68, T69, T70, T72, flatA_in_ga(.(T69, T70), T72))
U4_ga(T44, T68, T69, T70, T72, flatA_out_ga(.(T69, T70), T72)) → flatA_out_ga(.(.(T44, .(T68, T69)), T70), .(T44, .(T68, T72)))
U3_ga(T44, T57, T59, flatA_out_ga(T57, T59)) → flatA_out_ga(.(.(T44, []), T57), .(T44, T59))
U2_ga(T35, T36, T37, T39, flatA_out_ga(.(T36, T37), T39)) → flatA_out_ga(.([], .(.(T35, T36), T37)), .(T35, T39))
U1_ga(T16, T18, flatA_out_ga(T16, T18)) → flatA_out_ga(.([], .([], T16)), T18)
FLATA_IN_GA(.([], .([], T16)), T18) → U1_GA(T16, T18, flatA_in_ga(T16, T18))
FLATA_IN_GA(.([], .([], T16)), T18) → FLATA_IN_GA(T16, T18)
FLATA_IN_GA(.([], .(.(T35, T36), T37)), .(T35, T39)) → U2_GA(T35, T36, T37, T39, flatA_in_ga(.(T36, T37), T39))
FLATA_IN_GA(.([], .(.(T35, T36), T37)), .(T35, T39)) → FLATA_IN_GA(.(T36, T37), T39)
FLATA_IN_GA(.(.(T44, []), T57), .(T44, T59)) → U3_GA(T44, T57, T59, flatA_in_ga(T57, T59))
FLATA_IN_GA(.(.(T44, []), T57), .(T44, T59)) → FLATA_IN_GA(T57, T59)
FLATA_IN_GA(.(.(T44, .(T68, T69)), T70), .(T44, .(T68, T72))) → U4_GA(T44, T68, T69, T70, T72, flatA_in_ga(.(T69, T70), T72))
FLATA_IN_GA(.(.(T44, .(T68, T69)), T70), .(T44, .(T68, T72))) → FLATA_IN_GA(.(T69, T70), T72)
flatA_in_ga([], []) → flatA_out_ga([], [])
flatA_in_ga(.([], []), []) → flatA_out_ga(.([], []), [])
flatA_in_ga(.([], .([], T16)), T18) → U1_ga(T16, T18, flatA_in_ga(T16, T18))
flatA_in_ga(.([], .(.(T35, T36), T37)), .(T35, T39)) → U2_ga(T35, T36, T37, T39, flatA_in_ga(.(T36, T37), T39))
flatA_in_ga(.(.(T44, []), T57), .(T44, T59)) → U3_ga(T44, T57, T59, flatA_in_ga(T57, T59))
flatA_in_ga(.(.(T44, .(T68, T69)), T70), .(T44, .(T68, T72))) → U4_ga(T44, T68, T69, T70, T72, flatA_in_ga(.(T69, T70), T72))
U4_ga(T44, T68, T69, T70, T72, flatA_out_ga(.(T69, T70), T72)) → flatA_out_ga(.(.(T44, .(T68, T69)), T70), .(T44, .(T68, T72)))
U3_ga(T44, T57, T59, flatA_out_ga(T57, T59)) → flatA_out_ga(.(.(T44, []), T57), .(T44, T59))
U2_ga(T35, T36, T37, T39, flatA_out_ga(.(T36, T37), T39)) → flatA_out_ga(.([], .(.(T35, T36), T37)), .(T35, T39))
U1_ga(T16, T18, flatA_out_ga(T16, T18)) → flatA_out_ga(.([], .([], T16)), T18)
FLATA_IN_GA(.([], .(.(T35, T36), T37)), .(T35, T39)) → FLATA_IN_GA(.(T36, T37), T39)
FLATA_IN_GA(.([], .([], T16)), T18) → FLATA_IN_GA(T16, T18)
FLATA_IN_GA(.(.(T44, []), T57), .(T44, T59)) → FLATA_IN_GA(T57, T59)
FLATA_IN_GA(.(.(T44, .(T68, T69)), T70), .(T44, .(T68, T72))) → FLATA_IN_GA(.(T69, T70), T72)
flatA_in_ga([], []) → flatA_out_ga([], [])
flatA_in_ga(.([], []), []) → flatA_out_ga(.([], []), [])
flatA_in_ga(.([], .([], T16)), T18) → U1_ga(T16, T18, flatA_in_ga(T16, T18))
flatA_in_ga(.([], .(.(T35, T36), T37)), .(T35, T39)) → U2_ga(T35, T36, T37, T39, flatA_in_ga(.(T36, T37), T39))
flatA_in_ga(.(.(T44, []), T57), .(T44, T59)) → U3_ga(T44, T57, T59, flatA_in_ga(T57, T59))
flatA_in_ga(.(.(T44, .(T68, T69)), T70), .(T44, .(T68, T72))) → U4_ga(T44, T68, T69, T70, T72, flatA_in_ga(.(T69, T70), T72))
U4_ga(T44, T68, T69, T70, T72, flatA_out_ga(.(T69, T70), T72)) → flatA_out_ga(.(.(T44, .(T68, T69)), T70), .(T44, .(T68, T72)))
U3_ga(T44, T57, T59, flatA_out_ga(T57, T59)) → flatA_out_ga(.(.(T44, []), T57), .(T44, T59))
U2_ga(T35, T36, T37, T39, flatA_out_ga(.(T36, T37), T39)) → flatA_out_ga(.([], .(.(T35, T36), T37)), .(T35, T39))
U1_ga(T16, T18, flatA_out_ga(T16, T18)) → flatA_out_ga(.([], .([], T16)), T18)
FLATA_IN_GA(.([], .(.(T35, T36), T37)), .(T35, T39)) → FLATA_IN_GA(.(T36, T37), T39)
FLATA_IN_GA(.([], .([], T16)), T18) → FLATA_IN_GA(T16, T18)
FLATA_IN_GA(.(.(T44, []), T57), .(T44, T59)) → FLATA_IN_GA(T57, T59)
FLATA_IN_GA(.(.(T44, .(T68, T69)), T70), .(T44, .(T68, T72))) → FLATA_IN_GA(.(T69, T70), T72)
FLATA_IN_GA(.([], .(.(T35, T36), T37))) → FLATA_IN_GA(.(T36, T37))
FLATA_IN_GA(.([], .([], T16))) → FLATA_IN_GA(T16)
FLATA_IN_GA(.(.(T44, []), T57)) → FLATA_IN_GA(T57)
FLATA_IN_GA(.(.(T44, .(T68, T69)), T70)) → FLATA_IN_GA(.(T69, T70))
No rules are removed from R.
FLATA_IN_GA(.([], .(.(T35, T36), T37))) → FLATA_IN_GA(.(T36, T37))
FLATA_IN_GA(.([], .([], T16))) → FLATA_IN_GA(T16)
FLATA_IN_GA(.(.(T44, []), T57)) → FLATA_IN_GA(T57)
POL(.(x1, x2)) = 2·x1 + 2·x2
POL(FLATA_IN_GA(x1)) = 2·x1
POL([]) = 0
FLATA_IN_GA(.(.(T44, .(T68, T69)), T70)) → FLATA_IN_GA(.(T69, T70))
FLATA_IN_GA(.(.(T44, .(T68, T69)), T70)) → FLATA_IN_GA(.(T69, T70))
POL(.(x1, x2)) = 1 + 2·x1 + 2·x2
POL(FLATA_IN_GA(x1)) = 2·x1